Nuprl Lemma : sorted_wf
0,22
postcript
pdf
T
:Type.
T
(
L
:
T
List. sorted(
L
)
Prop)
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
||
as
||
,
P
&
Q
,
i
j
<
k
,
P
Q
,
False
,
A
,
A
B
,
{
i
..
j
}
,
S
T
,
l
[
i
]
,
Prop
,
sorted(
L
)
Lemmas
int
seg
wf
,
le
wf
,
select
wf
,
length
wf1
origin
T:Type. T 
(L:T List. sorted(L) 
Prop) T:Type. T (L:T List. sorted(L) Prop) Tx:A. B(x)
j < k Q
AB
} T